(0) Obligation:

Clauses:

d(+(U, V), X, +(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(-(U, V), X, -(DU, DV)) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(*(U, V), X, +(*(DU, V), *(U, DV))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(/(U, V), X, /(-(*(DU, V), *(U, DV)), ^(V, 2))) :- ','(!, ','(d(U, X, DU), d(V, X, DV))).
d(^(U, N), X, *(DU, *(N, ^(U, N1)))) :- ','(!, ','(integer(N), ','(is(N1, -(N, 1)), d(U, X, DU)))).
d(-(U), X, -(DU)) :- ','(!, d(U, X, DU)).
d(exp(U), X, *(exp(U), DU)) :- ','(!, d(U, X, DU)).
d(log(U), X, /(DU, U)) :- ','(!, d(U, X, DU)).
d(X, X, 1) :- !.
d(C, X, 0).
main :- ','(expression(X), ','(d(X, x, Y), write(Y))).
expression(+(Exp, -(Exp, *(Exp, /(Exp, *(Exp, /(Exp, Exp))))))) :- value(Exp).
value(/(+(*(3, x), -(*(4, *(exp(^(x, 3)), log(^(x, 2)))), 2)), +(-(*(3, x)), /(5, +(exp(^(x, 4)), 2))))).

Query: deriv(a,g,g)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:


Clauses:


Afs:

(3) TPisEmptyProof (EQUIVALENT transformation)

There are no more dependency triples. Hence, the dependency triple problem trivially terminates.

(4) YES